$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$T$)\} .
\\[0ex]($\neg$($\uparrow$$x$ changed before $e$)) $\Rightarrow$ (($x$ when $e$) = $x$ initially@loc($e$)  $\in$ $T$)